internalization and categorical algebra
algebra object (associative, Lie, …)
symmetric monoidal (∞,1)-category of spectra
An algebraic theory is a concept in universal algebra that describes a specific type of algebraic gadget, such as groups or rings. An individual group or ring is a model of the appropriate theory. Roughly speaking, an algebraic theory consists of a specification of operations and laws that these operations must satisfy.
Traditionally, algebraic theories were described in terms of logical syntax, as first-order theories whose signatures have only function symbols, no relation symbols, and all of whose axioms are equational law?s (universally quantified equations between terms built out of these function symbols). Such descriptions may be viewed as presentations of a theory, analogous to generators and relations as presentations of groups. In particular, different logical presentations can lead to equivalent mathematical objects.
In his thesis, Bill Lawvere undertook a more invariant description of (finitary) algebraic theories. Here all the definable operations of an algebraic theory, or rather their equivalence classes modulo the equational axioms imposed by the theory, are packaged together to form the morphisms of a category with finite products, called a Lawvere theory. None of these operations are considered “primitive”, so a Lawvere theory doesn’t play favorites among operations.
This article is about generalized Lawvere theories. The article Lawvere theory treats the traditional notion of finitary, single-sorted Lawvere theories, with worked examples. The core of the present article is a working out of the precise connection between infinitary (multi-sorted) Lawvere theories and monads.
Intuitively, a Lawvere theory is the “generic category of products equipped with an object of given algebraic type ”. For example, the Lawvere theory of groups is what you get by assuming a category with products and with a group object inside, and nothing more; can be considered “the generic group”. Every object in the Lawvere theory is a finite power of the generic object . The morphisms are nothing but the -ary operations it is possible to define on .
In other words, if we abstract away from the usual set-theoretic semantics, and consider a model for the theory of groups to be any category with finite products together with a specified group object inside, then the Lawvere theory of groups becomes a universal model of the theory, and carries all the information of the theory but independent of a particular presentation. In this way, theories and models of a theory are placed on an equal footing. A model of a Lawvere theory in a category with products is nothing but (i.e., is equivalent to) a product-preserving functor ; where the generic object is sent to is the given model of in . If is the Lawvere theory of groups, then a product-preserving functor is tantamount to an ordinary group.
The actual categorical construction of a Lawvere theory is described very easily and elegantly: it is the category opposite to the category of (finitely generated) free algebras of the theory. The free algebra on one generator becomes the generic object.
If theories and models are placed on an equal footing, then what feature sets “theories” per se apart? In some very abstract sense, any category with products could be considered a theory, where the -models in are product-preserving functors . Sometimes this is a useful point of view, but it is far removed from traditional syntactic considerations. To give a more “honest” answer, we remember that an ordinary (finitary, single-sorted) algebraic theory a la Lawvere is generated from a single object , and that every other object should be (at least up to isomorphism) a finite power . The exponent serves to keep track of arities of operations.
The generic “category of arities” is, in the finitary case, the category opposite to the category of finite sets (opposite because the appears contravariantly in powers ). This is also the Lawvere “theory of equality”, or if you prefer the theory generated by an empty signature. The answer to the question “what sets theories apart” is that a Lawvere theory should come equipped with a product-preserving functor
that is essentially surjective (each object of is isomorphic to for some arity ). As we see below, this definition is a cornerstone to a very elegant theory of algebraic theories.
Lawvere’s program can be extended to cover many theories with infinitary operations as well. In the best-behaved case, one has algebraic theories involving only operations of arity bounded by some cardinal number — or, more precisely, belonging to some arity class — and these can be understood category-theoretically with a suitable generalization of Lawvere theories. In this bounded case, the Lawvere theory can be described by a small category, and the category of models will be very well behaved, in particular it is a locally presentable category. In such cases there is a satisfying duality between syntax and semantics along the lines of Gabriel-Ulmer duality.
Lawvere’s program can to some degree be extended further: one can work with Lawvere theories which are locally small (not just small) categories. Here, the theory might not be bounded, but at least there is only a small set of operations of each arity. Examples of such large theories include
The theory of algebras with arbitrary sums (one model of which is ),
The theory of sup-lattices, in which there is one operation of each arity, and
The theory of compact Hausdorff spaces, where the operations are parametrized by ultrafilters.
These examples go outside the bounded (small theory) case. Locally small theories in this sense are co-extensive with the notion of monad (on ): there is a free-forgetful adjunction between and the category of models, and algebras of the theory are equivalent to algebras of the monad.
In the worst case, there are algebraic theories where the number of definable operations explodes, so that there may be a proper class of operations of some fixed arity. In this case there are no free algebras, and Lawvere’s reformulation no longer applies. An example is the theory of complete Boolean algebras. (Note: category theorists who define a category over sets to be algebraic if it is monadic would therefore not consider the variety of algebras in such cases to be “algebraic”).
Further commentary on these aspects may be found in the dozen or so comments in this thread, dated April 13 - May 7, 2009.
In summary, then, here is the connection between the logical and categorial descriptions, based on Johnstone, §§3.7&8. Say that a category is:
Then any small algebraic category is algebraic, and any algebraic category is large algebraic, but neither implication may be reversed.
Lawvere theories can also be generalized to handle multi-sorted operations. If is a set of sorts, then multisorted operations are of the form
so that arities are functors , where is seen as a discrete category. Thus, an infinitary multi-sorted Lawvere theory involves an essentially surjective product-preserving functor
and the development goes through very much as in the single-sorted case.
See generalized algebraic theory.
For the moment we discuss the single-sorted case. The many-sorted case should be a straightforward extension.
For any cardinal , let be a set of that cardinality (sometimes we just use ).
A Lawvere theory or algebraic theory is a locally small category with small products that is equipped with an object such that the (unique-up-to-isomorphism) product-preserving functor
is essentially surjective.
Algebraic theories can be extended or specialized in various directions. Here are a few variations on the theme.
Essentially algebraic theories allow for partially-defined operations. Just as finitary algebraic theories can be understood as Lawvere theories, which live in the doctrine of cartesian monoidal categories, so finitary essentially algebraic theories can be understood by a generalisation to finitely complete categories.
Multi-sorted theories? allow for more than one sort or type in the theory.
Let be a set whose elements are called sorts. There is a canonical map
which sends to the object in . Each object of may be thought of as a monomial term where is a set of variables indexed by , although it makes better sense to think of it that way when it is regarded as an object of .
Thus, objects of are pairs , where is any set, and morphisms are functions such that , or for all . Clearly, has small products. In fact, any object of is a product of objects of the form .
is the free category with small products generated by the set .
Let be a category with small products and let be any function. Define a functor
so that is taken to . It is immediate that is a product-preserving functor and is, up to unique isomorphism, the unique product-preserving functor that extends .
A multi-sorted algebraic theory over the set of sorts consists of a locally small category with small products, , together with a sort assignment such that the product-preserving extension
is essentially surjective. An operation of arity in is a morphism of the form in . If has small products, a model of in is a product-preserving functor . A homomorphism of models is simply a natural transformation between product-preserving functors.
It violates the principle of equivalence, but is nevertheless harmless and sometimes convenient, to suppose is an isomorphism on objects, since we can define to have the same objects as and define hom-sets by . Then, the functor evidently factors as
where the second functor is an equivalence, so we may as well work with the functor .
Commutative algebraic theories are (single-sorted) algebraic theories for which each operation is an algebra homomorphism. These form an important subclass. Their categories of models are closed: the hom sets have a natural model-structure (algebra-structure), and the enriched Hom-functor has a left adjoint, tensor product.
The theory of -modules for a fixed commutative ring is perhaps the most familiar example. The theory of complete lattices and supremum-preserving functions is an interesting non-finitary example.
We flesh out the relationships between algebraic theories and monads, starting from the most general situation and then adding conditions to cut down on the size of theories. The term “Lawvere theory” as used here will mean a large (but locally small) infinitary Lawvere theory. (Under this relation ordinary finitary Lawvere theories correspond to finitary monads.)
Suppose is a (locally small, multi-sorted) Lawvere theory, so we have a product-preserving functor
which we may assume to be the identity on objects. We define an adjoint pair between the category of models , consisting of product-preserving functors and transformations between them, and the category . We also denote this model category by .
Observe that is a Lawvere theory which is the theory of -multi-sorted sets,
where the first equivalence obtains precisely because is the free category with products generated by .
Let be the Yoneda embedding, taking to the product-preserving functor .
The functor
is left adjoint to the functor
(using the remark above).
We must exhibit a natural isomorphism
where indicates the hom-functor on the functor category . The left side is naturally isomorphic to
by the Yoneda lemma. The right side is isomorphic to
where is the canonical embedding. Now both and are product-preserving functors , so to check these functors are isomorphic, it suffices (by the universal property of to check they give isomorphic results when restricted along :
However, because is itself a Yoneda embedding , the last isomorphism is just an instance of the Yoneda lemma, and this concludes the proof.
The monad of a Lawvere theory is the monad associated with this adjunction.
Now let be a monad on , with unit and multiplication .
The large Lawvere theory of is the opposite of the Kleisli category, .
The left adjoint is coproduct-preserving, so we have a product-preserving functor
which is a bijection on the classes of objects. Therefore is indeed a (large, multi-sorted) Lawvere theory.
Let be a monad on . The monad associated with the theory is isomorphic to .
In other words, we claim the monad of the adjunction
is isomorphic to . Now the functor is left adjoint to the underlying functor , and the underlying monad there is of course . It is obvious that the composite
takes an object to
and since the equivalence is adjoint to the yoneda embedding, it takes to . This proves the claim.
In the other direction, we have
Let be an -sorted Lawvere theory. Then the Lawvere theory of the monad of is equivalent to .
We assume for convenience that the product-preserving functor is the identity on the class of objects.
We need to exhibit a comparison functor , where is the monad of . Such a comparison functor exists provided that has a left adjoint whose associated monad is isomorphic to . Now the composite
sends an object of to the product-preserving functor which, by the remark above, is represented by an object of which we denote as . In other words we have a natural isomorphism
and by the usual Yoneda yoga, we obtained a functor which is left adjoint to . The monad is, by definition (see theorem 1) the monad associated with the adjoint pair .
We thus obtain the comparison functor , and it is the identity on objects. On hom-sets it is given by the natural isomorphism
and hence the comparison functor is an equivalence.
Each algebra of the monad gives rise to a model of the Lawvere theory:
and similarly a morphism of algebras gives rise to a homomorphism , so that we have a functor . This functor is an equivalence.
It is convenient to proceed as follows. By Theorem 2, the underlying functor
has a left adjoint such that the associated monad is , and this yields a comparison functor
is an equivalence.
In outline, this proceeds as follows:
is essentially surjective, because if is a -algebra, then is a product-preserving functor such that .
is full, because any algebra map gives rise to a model homomorphism .
is faithful. For this it suffices to prove that the underlying functor
is faithful. Let be a morphism of . Now every object of is a product of objects in the image of
From the naturality of the diagram
and the fact that preserves products, we see that the component of at is uniquely determined from the components as ranges over the image of , in other words that the functor defined by is faithful.
Thus is an equivalence, with essential inverse .
Ring theory is a branch of mathematics with a well-developed terminology. A ring determines and is determined by an algebraic theory, whose models are left -modules and whose -ary operations have the form
for some n-tuple of elements of . We may call such an algebraic theory annular. The pun model/module is due to Jon Beck. The notion that an algebraic theory is a generalized ring is often a fertile one, that automatically provides a slew of suggestive terminology and interesting problems. Many fundamental ideas of ring/module-theory are simply the restriction to annular algebraic theories of ideas that apply more widely to algebraic theories and their models.
Let us denote the category of models and homomorphisms (in ) of an algebraic theory by . Then compare the following to their counterparts in ring theory:
algebraic theory / Lawvere theory / 2-Lawvere theory / (∞,1)-algebraic theory
finitely complete category, cartesian functor, cartesian logic, cartesian theory
regular category, regular functor, regular logic, regular theory, regular coverage, regular topos
coherent category, coherent functor, coherent logic, coherent theory, coherent coverage, coherent topos
geometric category, geometric functor, geometric logic, geometric theory
Ernest G. Manes, Algebraic Theories, Springer (1976) [doi:10.1007/978-1-4612-9860-1]
Jiří Adámek, Jiří Rosický, Enrico Vitale, Algebraic theories, Cambridge University Press (2011) [doi:10.1017/CBO9780511760754, pdf]
B. Badzioch, “Algebraic Theories in Homotopy Theory”, Annals of Mathematics, 155, 895–913 (2002).
Andreas Nuyts, Understanding Universal Algebra Using Kleisli-Eilenberg-Moore-Lawvere Diagrams, note
For a framework to compare different notions of algebraic theory see
Last revised on December 2, 2023 at 11:28:04. See the history of this page for a list of all contributions to it.